a, b, c, d:. a  b  c < d  a + c < b + d 

latex

Definitions	P & Q, T, P  Q, P  Q, , True, t  T, P  Q, x:A. B(x)
Lemmas	qadd wf, qless transitivity 2 qorder, grp op preserves le qorder, qadd com, true wf, squash wf, grp op preserves lt qorder, rationals wf, qle wf, qless wf